Nuprl Definition : qrng
11,40
postcript
pdf
qrng
== <rationals
==
,
x
,
y
. qeq(
x
;
y
)
==
,
x
,
y
. q_le(
x
;
y
)
==
,
x
,
y
.
x
+
y
==
, 0
==
,
x
.-(
x
)
==
,
x
,
y
.
x
*
y
==
, 1
==
,
x
,
y
. if qeq(
y
; 0) then inr
else inl qdiv(
x
;
y
) fi >
latex
clarification:
qrng
== <rationals
==
,
x
,
y
. qeq(
x
;
y
)
==
,
x
,
y
. q_le(
x
;
y
)
==
,
x
,
y
.
x
+
y
==
, 0
==
,
x
.(-1) *
x
==
,
x
,
y
.
x
*
y
==
, 1
==
,
x
,
y
. if qeq(
y
; 0) then inr
else inl qdiv(
x
;
y
) fi >
latex
Definitions
rationals
,
q_le(
r
;
s
)
,
r
+
s
,
-
n
,
r
*
s
,
<
a
,
b
>
,
x
.
A
(
x
)
,
if
b
then
t
else
f
fi
,
qeq(
r
;
s
)
,
#$n
,
inr
x
,
,
inl
x
,
qdiv(
r
;
s
)
FDL editor aliases
qrng
origin